Playing with State-Based Models for Designing Better Algorithms
Identifieur interne : 000028 ( Main/Exploration ); précédent : 000027; suivant : 000029Playing with State-Based Models for Designing Better Algorithms
Auteurs : Dominique Mery [France]Source :
English descriptors
- mix :
Abstract
State-based models provide a very convenient framework for analysing, verifying, validating and designing sequential as well as concurrent or distributed algorithms. Each state-based model is considered as an abstraction, which is more or less close to the target algorithmic entity. The problem is then to organise the relationship between an initial abstract state-based model expressing requirements and a final concrete state- based model expressing a structured algorithmic state-based model. A simulation (or refinement) relation between two state-based models allows to structure these mod- els from an abstract view to a concrete view. Moreover, state-based models can be extended by assertion languages for expressing correctness properties as pre/post spec- ification, safety properties or even temporal properties. In this work, we review state- based models and play scores for verifying and designing concurrent or distributed algorithms. We choose the Event-B modelling language for expressing state-based models and we show how we can play Event-B scores using Rodin and methodologi- cal elements to guarantee that the resulting algorithm is correct with respect to initial requirements. First, we show how annotation-based verification can be handled in the Event-B modelling language and we propose an extension to handle the verification of concurrent programs. In a second step, we show how important is the concept of refinement and how it can be used to found a methodology for designing concurrent programs using the coordination paradigm.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 003B98
- to stream Hal, to step Curation: 003B98
- to stream Hal, to step Checkpoint: 000028
- to stream Main, to step Merge: 000028
- to stream Main, to step Curation: 000028
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Playing with State-Based Models for Designing Better Algorithms</title>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Mery</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno>
<idno type="IdUnivLorraine">[UL]100--</idno>
<orgName>Université de Lorraine</orgName>
<orgName type="acronym">UL</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-lorraine.fr/</ref>
</desc>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01316026</idno>
<idno type="halId">hal-01316026</idno>
<idno type="halUri">https://hal.inria.fr/hal-01316026</idno>
<idno type="url">https://hal.inria.fr/hal-01316026</idno>
<date when="2016-05-14">2016-05-14</date>
<idno type="wicri:Area/Hal/Corpus">003B98</idno>
<idno type="wicri:Area/Hal/Curation">003B98</idno>
<idno type="wicri:Area/Hal/Checkpoint">000028</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000028</idno>
<idno type="wicri:Area/Main/Merge">000028</idno>
<idno type="wicri:Area/Main/Curation">000028</idno>
<idno type="wicri:Area/Main/Exploration">000028</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Playing with State-Based Models for Designing Better Algorithms</title>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Mery</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno>
<idno type="IdUnivLorraine">[UL]100--</idno>
<orgName>Université de Lorraine</orgName>
<orgName type="acronym">UL</orgName>
<date type="start">2012-01-01</date>
<desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-lorraine.fr/</ref>
</desc>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Algorithm</term>
<term>Coordination</term>
<term>Languages</term>
<term>Modelling</term>
<term>Refinement</term>
<term>Verification</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">State-based models provide a very convenient framework for analysing, verifying, validating and designing sequential as well as concurrent or distributed algorithms. Each state-based model is considered as an abstraction, which is more or less close to the target algorithmic entity. The problem is then to organise the relationship between an initial abstract state-based model expressing requirements and a final concrete state- based model expressing a structured algorithmic state-based model. A simulation (or refinement) relation between two state-based models allows to structure these mod- els from an abstract view to a concrete view. Moreover, state-based models can be extended by assertion languages for expressing correctness properties as pre/post spec- ification, safety properties or even temporal properties. In this work, we review state- based models and play scores for verifying and designing concurrent or distributed algorithms. We choose the Event-B modelling language for expressing state-based models and we show how we can play Event-B scores using Rodin and methodologi- cal elements to guarantee that the resulting algorithm is correct with respect to initial requirements. First, we show how annotation-based verification can be handled in the Event-B modelling language and we propose an extension to handle the verification of concurrent programs. In a second step, we show how important is the concept of refinement and how it can be used to found a methodology for designing concurrent programs using the coordination paradigm.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
</list>
<tree><country name="France"><noRegion><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Mery</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000028 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000028 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= Hal:hal-01316026 |texte= Playing with State-Based Models for Designing Better Algorithms }}
This area was generated with Dilib version V0.6.33. |